Reachability anaysis may also be performed when the components are specified as extended state machines. For the "finite state aspect" of the specifications, the reachability analysis approach discussed above can be used, while the difficulty comes from the conditions that must be satisfied by the interaction parameters and values of the additional state variables. This involves usually to write these conditions as assertions associated with the different states of the "finite state aspect" of the global model, and then verifying that these assertions hold in all reachable states of the system. Two approaches may be used toverify that these assertions always hold::
The main difficulty of reachability is the so-called state space explosion, meaning that the number of reachable states grows very large. There are three reasons why often the number of reachable states is too big to be manageable, even with powerful tools:
This state space explosition represents a problem for reachability analysis, since it is necessary to remember which global states have already been encountered (and analysed). When a new transition from the currently explored state is executed, one has to record the next global state reached and determine whether it was encountered before, or whether it is a new global state (that must be explored). The easiest way is to store all global states that have been encountered together with a boolean flag which indicates whether all transitions from this state have already been explored or not. Each global state contains the states of each component, all messages in transit (i.e. in queues) together with their parameter values, and the values of the local state variables of all components. Therefore each global state may easily require a good number of octets to store. Since memory is limited, the number of states that can be explored is limited.
The number of reachable states in not only often very large, in many cases it is even infinite. Consider for instance an FSM that has a spontaneous transition that sends a message to its partner and loops back to the same state. In this case, the number of message that may be in transit at any given time is not bounded. Therefore the number of global reachable states is infinite. Clearly such spaces cannot be covered completely. The question is: Is it necessary to explore global states with an arbitrary number of messages in transit ? - In practice, one usually explores only states with a number of messages in transit within a bound. But it is not clear what such a bound should be. Sometimes the reachability analysis shows (if a complete exploration has been done) that the number of messages in transit from a given source component to some given destination component is always less than same bound. However, it has been shown that the problem of deciding whether two given communication state machines may get into a deadlock state is undecidable. Also the question whether the number of messages in transit remains bounded is undecidable.
Holzmann (the author of Spin) proposed a method for minimizing the required memory for remembering which global state has already been analyzed (using only one bit per state). In his paper of 1986 he proposed to consider the representation of a global state as the address (in memory) for a single bit. This bit is set to 1 when the state has been explored. When a new transition is explored, the bit at the address indicated by the next state is checked to see if it has the value 1 (which means that the state was encountered before). If the state space is large, there may still not be enough memory to store a bit for all possible global states (note that not all possible global states will be reachable- therefore most bits will remain with a value 0). Therefore Holzmann proposed to hash the value of the global state into the address space of the available memory. This is called state hashing. - This, however, is not perfect, since different global states may hash to the same value, which means that if the bit for the next state explored is already set to 1, it means that either this state was encountered before, or there is a hash conflict with another global state that was encountered before (but the currently explored state is actually new). Since one cannot distinguish between these two cases, one assumes that the explored state was encountered before and will not be further explored. Therefore this leads to randomly partial exploration of the reachable state space of the system under analysis.
Analysis methods that do not construct the whole reachable global state space, but only travel through the whole space (for instance through a depth-first search) and simultaneously check the interesting properties are called “on-the-fly” analysis methods. In opposition, traditional methods construct the whole state space and then check the interesting properties.
The following approaches have been proposed to reduce the effect of state space explosion:
Created: October 2014